$\forall$$b$:$\mathbb{N}$, $f$:(int\_seg(0; $b$)$\rightarrow\mathbb{B}$).
\\[0ex]($\exists$$n$:int\_seg(0; $b$). ($\uparrow$($f$($n$))))
\\[0ex]$\Rightarrow$ guard((($\uparrow$($f$(mu($f$)))) $\wedge$ ($\forall$$i$:int\_seg(0; $b$). ($i$ $<$ mu($f$)) $\Rightarrow$ ($\neg$($\uparrow$($f$($i$)))))))